$\forall$$A$:Type, $f$:($A$$\rightarrow$($A$ + Top)), $x$:$A$, $n$:$\mathbb{N}$.
\\[0ex]($\uparrow$can{-}apply($f$;$x$)) $\Rightarrow$ (($f$\^{}$n$+1($x$)) $\sim$ ($f$\^{}$n$(do{-}apply($f$;$x$))))